$\forall$$S$, $V$:Type, $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), $l$:IdLnk, $s$:$S$, $v$:$V$, $L$:($t$:Id$\times$($S$$\rightarrow$$V$$\rightarrow$($M$($l$,$t$) List))) List.
\\[0ex]tagged{-}messages($l$;$s$;$v$;$L$) $\in$ \{$m$:Msg($M$)$\mid$ mlnk($m$) $=$ $l$ \} List